The present invention relates generally to the field of functional verification of digital circuit designs. More specifically, the present invention relates to the field of formal verification of a digital circuit design and verifying the behavior of a circuit model to satisfy specified properties.
Recent increases in the complexity of modern integrated circuits have exacerbated the difficulty of verifying design correctness. The verification phase of a typical integrated circuit design project consumes approximately 70–80% of the total time and resources dedicated to a project. Flaws in the design that are not found during the verification phase have significant economic impact in terms of increased time-to-market and reduced profit margins.
A typical design flow for integrated circuit design includes many steps that proceed sequentially, with each step depending on the results of the previous steps. Consequently, when a flaw is discovered in a step, all the previous steps must be repeated, often at a significant cost. Hence, it is highly desirable to find and fix design flaws as early as possible in a design flow.
Traditionally, simulation-based techniques have been used to verify design correctness. Transistor-level simulation based techniques were used in the early 1970s and logic gate-level simulation based techniques were used in the late 1980s. As the complexity of designs increased with the passage of time, drawbacks associated with these techniques came into light. These techniques became less effective because of their inability to completely and quickly verify large designs. A popular alternative is the use of Register Transfer Language (RTL)-level simulation. Contemporary verification and debugging tools use various levels of abstractions for defining design specifications. These abstractions are expressed in high-level description languages. High-level description languages provide a number of functionalities for analyzing and verifying a design while performing simulation. For example, a designer can navigate the design hierarchy, view the RTL source code, and set breakpoints on a statement of an RTL source code to stop the simulation. Also, line numbers are provided in the RTL source code to identify different lines and statements. Further, the verification and debugging tools often support viewing and tracing variables and some times even signal values. These RTL-level simulation tools typically also offer these and other types of RTL debugging functionalities.
The verification tools as mentioned above typically follow a design flow. In the first step of the design flow, the conceptual nature of the integrated circuit is determined. The desired functionality of a circuit is expressed as a collection of properties or specifications, and possibly as a model of the behavior in a high-level language such as C++. The RTL model of the digital circuit is built based upon knowledge of the specifications or the high-level model. The RTL model is expressed in a hardware description language (HDL) such as Verilog available from Cadence Design Systems, Inc. of Santa Clara, Calif. or VHDL available from IEEE of New York, N.Y. Many other steps such as synthesis, timing optimization, clock tree insertion, place and route, etc., yield subsequent transformations of the design. These transformations eventually result in a set of masks that are fabricated into integrated circuits. The current invention is targeted at finding design flaws in the RTL model of the design, which is a very early phase of the design flow.
In the design flow, creation of RTL source code is followed by verification in order to check the compliance of the RTL source code to the design specifications. Three approaches commonly used to verify the design at the RTL level are simulation, emulation and formal methods.
Simulation is one of the most prevalent methods used to determine whether the design is in accordance with the specifications by simulating the behavior of the RTL model. The simulation process uses RTL source code and a “Test Bench” to verify a design. The Test Bench contains a subset of all possible inputs to the circuit/logic. For an ‘n’ input circuit, there are 2″ possible inputs at any given time. For large n, e.g., for a complex design, the number of possible input sequences becomes prohibitively large. To simplify this, only a subset of all possible input sequences is described in any given Test Bench. An example of such a tool is NC-Verilog from Cadence Design Systems, Inc. of Santa Clara, Calif. To simulate the RTL model, a Test Bench must be created to provide appropriate input stimulus to the RTL model. Creating the Test Bench is a time consuming process. The process of simulating the Test Bench is also time consuming. Furthermore, it is effectively impossible to create enough test cases to completely verify that the specified properties of the design are true. This is because of the sheer number of possible input sequences, and also because it requires in-depth knowledge and tremendous creativity on the part of the Test Bench creator to imagine the worst-case scenarios.
An increasingly popular alternative is to use formal methods to completely verify properties of a design. Formal methods use mathematical techniques to prove that a design property is either always true, or to provide an example scenario (referred to as a counterexample) demonstrating that the property is false. One category of tools using formal methods to verify properties are known as Model Checkers. An example of a conventional model checking tool is the Formal-Check tool from Cadence Design Systems, Inc. of Santa Clara, Calif.
FIG. 1 shows an example of a property 120 and an environmental constraint 118 that could be applied to a circuit model 100. Property 120 specifies the behavior of the output signals (OUT_0 110, OUT_1 112, PREV_OUT_0 114, PREV_OUT_1 116). Environmental constraint 118 is a boolean expression that specifies constraint on the input signals (X_0 102, X_1 104, X_2 106), as described in greater detail below.
When the conventional method is applied to verify the property of a circuit model, there are three possible outcomes: (1) The system determines that the property is true for all input sequences that satisfy the set of environmental constraints. (2) The system is unable to make a determination due to lack of computing resource (time or memory). (3) The system determines that the property is false. In the latter case, the conventional system produces a counterexample that satisfies the set of environmental constraints, but for which the property fails to be true.
Several issues inhibit the widespread use of model checking. One issue is performance. Resources used to perform verification are typically exponentially related to the number of registers in the circuit model. This is referred to as the “state space explosion” problem. Many conventional Model Checkers analyze the entire design before proving a particular property. The complexity and size of modern integrated circuits, combined with the state space explosion problem, make it impossible to use such Model Checkers on large designs.
Instead of analyzing the entire design, other conventional Model Checkers analyze the portion of the design relevant to a particular property from a structural point of view. This includes all portions of the design between the signals relevant to the property and the primary inputs. An example of a conventional system that implements this property-dependent design analysis is the COSPAN model checking engine referred to in R. P. Kurshan, “Formal Verification in a Commercial Setting”, Design Automation Conference, pp. 258–262, June 1997, Anaheim, Calif. However, even the property-relevant portion of the design can be very large. Thus, in this case the state space explosion problem can result in severe performance problems.
Another issue is that no conventional system permits complete control over the region of the circuit model to be examined when verifying a particular property. The user typically resorts to manually modifying the design by removing and replacing parts of the design in order to determine if a property is true. An example of this design modification technique is described in S. G. Govindaraju et al., “Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking”, IEEE International Conference on Computer-Aided Design, pp. 115–119, November 2000. This modification of the design introduces the possibility of human error and requires additional steps.
Conventional formal verification techniques attempt to fully automate the formal verification process, and the primary flow usually does not involve getting inputs from the user. The primary interaction from the user is for the user to provide appropriate environmental constraints. However, a user that is used to running simulation may not know how to provide environmental constraints for a formal tool, and there may be a wide range of possible assumptions, some lead to an efficient formal analysis, some lead to incomplete proof.
In addition, even if the user has a chance to provide detailed guidance to the formal verification process, a user that is not an expert in formal verification may not know enough about the formal verification algorithm to provide the right inputs to the tool. Furthermore, at each interactive step, there may be a wide range of possible actions; without generating guidance from the tool for the user, the user may specify actions that have adverse effect to the performance of the formal verification process.
Accordingly, what is needed is a system and a method that (1) verifies a circuit model in a short duration of time, (2) automatically verifies a circuit model while permitting complete control over the region of the circuit model to be examined and environmental conditions to be applied, and (3) provides the user with information to evaluate the cost and effect of modifying the region of the circuit model to be examined and/or adding the environmental constraints (assumptions) to be applied.